:- module(concrete,[sem_start/2]).
:- use_module(library(lists)).
:- use_module(library(charsio)).
%:- use_module(abc_parser).
:- use_module(avm_objects).

:-use_module('abc_parser.yap').

print_tabs(0).
print_tabs(N) :-
	N > 0,
	format('~t',[]),
	NewN is N-1,
	print_tabs(NewN).

% Used to generate a list of tt values
top_list([_Var|R]) :- top_list(R).
top_list([]).

initialize_start_state(S0) :-
	EE =.. [env,ScopeStack,OperandStack,RegisterFile],
	H = [],
	ScopeStack = [],
	OperandStack = [],
	RegisterFile = [],
	S0 = state(H,[EE], [], automaton(0)).

chop_list_until_nth2(List,0,List).
chop_list_until_nth2([_I1|Items],N,NewList) :- 
	NewN is (N-1),
	chop_list_until_nth2(Items,NewN,NewList).

chop_2(0, NewOp, NewOp, FullList, FullList).
chop_2(Count, [N, V | OpStack], NewOp, List, [(N-V) | List]) :-
	NewCount is (Count-1),
	chop_2(NewCount, OpStack, NewOp, [(N-V) | List], FullList).

cutmember(X,[X|_]) :- !.
cutmember(X,[_|L]) :- cutmember(X,L).

get_method2(MC, [M | _], M) :-
	M =.. [method_body,MC,_MS1,_LC1,_ISD1,_MSD1,_CL1,_NInsList,_EC1,_E1,_TC1,_T1].
get_method2(MC, [M | MT], MF) :-
	get_method2(MC, MT, MF).

get_jump_target(N, NIC, OInsList, CC, CC) :-

	nth0(NIC, OInsList, Ins1),
	nth0(CC, OInsList, Ins2),
	Ins1 = (L1 - _I1),
	Ins2 = (L2 - _I2),
	N is (L2-L1).

get_jump_target(N, NIC, OInsList, CC, FinalC) :-

	nth0(NIC, OInsList, Ins1),
	nth0(CC, OInsList, Ins2),
	Ins1 = (L1 - _I1),
	Ins2 = (L2 - _I2),

	( (N >= 0) ->
		NextCC is (CC+1)
	;
		NextCC is (CC-1)
	),

	get_jump_target(N, NIC, OInsList, NextCC, FinalC).

	
get_jump_path(PI, NPI, Offset, CL, NCL, Pos, Neg, WAST) :-
	PI =.. [path_info, OMN, OIC, PIP],
	writeln(PI),
	writeln(PIP),
	Mask is (PIP /\ 1),
	NewPIP is (PIP >> 1),

	writeln(PI),
	writeln(Offset),

	( (Mask = 1) ->
		% Do the branch
		b_getval(WAST, AST),
		abc_parser:getABC(method_bodies, AST, Methods),
		get_method2(OMN, Methods, Meth),
		Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,OInsList,_EC1,_E1,_TC1,_T1],
		NextIC is (OIC+1),
		get_jump_target(Offset, NextIC, OInsList, NextIC, NIC),

		NC = Pos,
		
		NPI =.. [path_info, OMN, NIC, NewPIP]
	;
		% Don't do the branch
		NewNIC is (OIC+1),
		NPI =.. [path_info, OMN, NewNIC, NewPIP],
		NC = Neg
	),

	((Pos = 0, Neg = 0) ->
		NCL = CL
	;

		((CL = []) ->
			NCL = [NC]
		;
			((CL = [NC|TempCL]) ->
				NCL = CL
			;
				NCL = [NC|CL]
			)
		)
	).
	
step_path_once(PI,NPI) :-
	PI =.. [path_info,MethodNum, InstrCount, OP],
	NextInstrCount is (InstrCount+1),
	NPI =.. [path_info,MethodNum, NextInstrCount, OP].

step_path_n(PI,N,NPI) :-
	PI =.. [path_info,MethodNum, InstrCount, OP],
	NPI =.. [path_info,MethodNum, (InstrCount+N), OP].


% add
instr(add, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :- 
	% Indicate to the verifier that the value on top of the stack is of any type
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [V1,V2|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [(V1+V2)|Os], RegisterFile].

% applytype
instr(applytype, [Type], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :- 
	% Indicate to the verifier that the value on top of the stack is of any type
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [V|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [V|Os], RegisterFile].

% astypelate
instr(astypelate, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': astypelate'),
	% Indicate to the verifier that the value on top of the stack is of any type
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [Value,Class|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [Value|Os], RegisterFile].

% bitand
instr(bitand, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': bitand'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	BA = V1 /\ V2,
	NewEE =.. [env, ScopeStack, [BA | OS] , RegisterFile].

% bitor
instr(bitor, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': bitor'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	BA = V1 \/ V2,
	NewEE =.. [env, ScopeStack, [BA | OS] , RegisterFile].

% call
instr(call, [ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': call'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%	get_property(Instr,next,NewInstr),
	% get_property(Instr,args,[_Namespace,ArgCount]),
	
	chop_list_until_nth2(OperandStack, ArgCount, NoArgOpStack),
	NoArgOpStack = [Function, Receiver | OpStack],

	write('callproperty: '), write(Function), write(' - '), writeln(Receiver),

	NewEE =.. [env, ScopeStack, [Value|OpStack], RegisterFile].

% callproperty
instr(callproperty, [_Index, ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': callproperty'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%	get_property(Instr,next,NewInstr),
	% get_property(Instr,args,[_Namespace,ArgCount]),
	
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, [Value|Rest], RegisterFile].

% callpropvoid
instr(callpropvoid, [Index, ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], NewTrace, NA), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': callpropvoid'),

	PI =.. [path_info, TMN, TIC, _TempPath],
	%((TMN = 971, TIC = 3) -> spy(chop_list_until_nth2); true),

	%	PI =.. [path_info, X1, X2, X3],
	%((X2 =:= 90) ->
	%	trace ; true),
	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,SC,Strings,NSC,Namespaces,_,_,MNC,Multinames)),
	

	nth(Index, Multinames, m_info(Kind, MultiNameQ)),

	writeln(MultiNameQ),

	((MultiNameQ = qname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqnamel(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = multiname(MNName, MNNamespace)) -> true ; true),
	((MultiNameQ = multinamel(MNName, MNNamespace)) -> true ; true),

	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	%write('OP Stack: '), writeln(OperandStack),

	

	chop_list_until_nth2(OperandStack, ArgCount, NoArgOpStack),

	NoArgOpStack = [Obj | OpStack],


	((MNNamespace = 0) ->
		NSName = '(*)'
	;
		nth(MNNamespace, Namespaces, namespace_info(_NSType,NSString)),
		%nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName)),
		((NSString = 0) ->
			NSName = ''
		;
			nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName))
		)
	),
	((MNName = 0) ->
		MethodName = '(*)'
	;
		nth(MNName, Strings, string_info(_SC, _SLI, MethodName))
	),

	NewTrace = [Index | Trace],

	% Check to see if the callpropvoid index matches a security relevent event
	b_getval(secrelindices, SecRel),
	(cutmember(Index,SecRel) ->
		A =.. [automaton, StateCount],
		NewStateCount is (StateCount+1),
		NA =.. [automaton, NewStateCount]
	;
		NA = A
	),

	writeln(NA),

	( (NSName = '', MethodName = 'init') ->
		% Get the last script
		b_getval(WAST, AST),
		abc_parser:getABC(script_count,AST,ScriptCount),
		abc_parser:getABC(scripts,AST,Scripts),
		nth(ScriptCount, Scripts, script_info(SCInit, _SCTC, _SCT)),
		step_path_once(PI, CPI),
		PI =.. [path_info, _MN, _IN, Path],
		NPI =.. [path_info, SCInit, 0, Path],
		NewEE =.. [env, ScopeStack, [CPI|OpStack], RegisterFile]

	;
		writeln('CallPropVoid to a system call, skipping...'),
		write('MethodName: '), write(MethodName), write(' ; MSName: '), writeln(MSName),
		step_path_once(PI, NPI),

		NewEE =.. [env, ScopeStack, OpStack, RegisterFile]
	).

% callsuper
instr(callsuper, [_Index, ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': callsuper'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%	get_property(Instr,next,NewInstr),
	% get_property(Instr,args,[_Namespace,ArgCount]),
	
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	NewEE =.. [env, ScopeStack, [Value|Rest], RegisterFile].

% callsupervoid
instr(callsupervoid, [Index, ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], NewTrace, NA), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': callsupervoid'),

	PI =.. [path_info, TMN, TIC, _TempPath],
	%((TMN = 131, TIC = 26) -> spy(chop_list_until_nth2); true),

	%	PI =.. [path_info, X1, X2, X3],
	%((X2 =:= 90) ->
	%	trace ; true),
	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,SC,Strings,NSC,Namespaces,_,_,MNC,Multinames)),
	

	nth(Index, Multinames, m_info(Kind, MultiNameQ)),

	writeln(MultiNameQ),

	((MultiNameQ = qname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqnamel(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = multiname(MNName, MNNamespace)) -> true ; true),
	((MultiNameQ = multinamel(MNName, MNNamespace)) -> true ; true),

	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	%write('OP Stack: '), writeln(OperandStack),

	

	chop_list_until_nth2(OperandStack, ArgCount, NoArgOpStack),

	NoArgOpStack = [Receiver | OpStack],

	((MNNamespace = 0) ->
		NSName = '(*)'
	;
		nth(MNNamespace, Namespaces, namespace_info(_NSType,NSString)),
		%nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName)),
		((NSString = 0) ->
			NSName = ''
		;
			nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName))
		)
	),
	((MNName = 0) ->
		MethodName = '(*)'
	;
		nth(MNName, Strings, string_info(_SC, _SLI, MethodName))
	),

	NewTrace = [Index | Trace],

	% Check to see if the callpropvoid index matches a security relevent event
	b_getval(secrelindices, SecRel),
	(cutmember(Index,SecRel) ->
		A =.. [automaton, StateCount],
		NewStateCount is (StateCount+1),
		NA =.. [automaton, NewStateCount]
	;
		NA = A
	),

	writeln(NA),

	( (NSName = '', MethodName = 'init') ->
		% Get the last script
		b_getval(WAST, AST),
		abc_parser:getABC(script_count,AST,ScriptCount),
		abc_parser:getABC(scripts,AST,Scripts),
		nth(ScriptCount, Scripts, script_info(SCInit, _SCTC, _SCT)),
		step_path_once(PI, CPI),
		PI =.. [path_info, _MN, _IN, Path],
		NPI =.. [path_info, SCInit, 0, Path],
		NewEE =.. [env, ScopeStack, [CPI|OpStack], RegisterFile]

	;
		writeln('CallPropVoid to a system call, skipping...'),
		write('MethodName: '), write(MethodName), write(' ; MSName: '), writeln(MSName),
		step_path_once(PI, NPI),

		NewEE =.. [env, ScopeStack, OpStack, RegisterFile]
	).

% coerce
instr(coerce, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': coerce'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%format('H = ~w, SS = ~w ,OS = ~w, RF = ~w~n', [H,ScopeStack,OperandStack,RegisterFile]),
	%	get_property(Instr,next,NewInstr),
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].
	
% coerce_a
instr(coerce_a, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': coerce_a'),
	step_path_once(PI,NPI),   
	% Indicate to the verifier that the value on top of the stack is of any type
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% coerce_s
instr(coerce_s, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': coerce_s'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [string(O)|Os], RegisterFile].
	
% construct
instr(construct, [ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': construct'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	chop_list_until_nth2(OperandStack, ArgCount, ObjStack),
	ObjStack = [Object | Rest],

	NewEE =.. [env, ScopeStack, [Value|Rest], RegisterFile].

% constructprop
instr(constructprop, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': constructprop'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%format('H = ~w, SS = ~w ,OS = ~w, RF = ~w~n', [H,ScopeStack,OperandStack,RegisterFile]),


	%	get_property(Instr,next,NewInstr),
	% get_property(Instr,args,[_NameSpace,ArgCount]),
	ArgList = [_NameSpace,ArgCount],
	length(ToPop,ArgCount+1),
	append(ToPop,Rest,OperandStack),
	%length(1, [Unbound]),
	NewEE =.. [env, ScopeStack, [_Unbound|Rest], RegisterFile].

% constructsuper
instr(constructsuper, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': constructsuper'), 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	ArgList = [ArgCount],
	chop_list_until_nth2(OperandStack, ArgCount, ObjStack),
	ObjStack = [Object | Rest],

	( (Object =.. [class,ClassName]) ->
		ClassNum is 0,
		%(\+(ClassName = '') ->
		%		writeln('Found Another Class Name in Construct Super!!!'),
		%		break),
		% Get the Class Info from the Classes Pool
		b_getval(WAST, AST),
		abc_parser:getABC(classes,AST,Classes),
		nth0(ClassNum, Classes, class_info(CInit,_TC,_TS)),
		step_path_once(PI,CPI),
		PI =.. [path_info, _MN, _IN, Path],
		NPI =.. [path_info, CInit, 0, Path],

		write('Creating Class From: '),
		writeln(PI),
		write('To Class: '),
		writeln(NPI),

		NewEE =.. [env, ScopeStack, [CPI|Rest], RegisterFile]

	;
		write('Object on top of Stack for ConstructSuper is not a class!  '),
		writeln(Object),
		break
	).

% convert_b
instr(convert_b, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': convert_b'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(O)|Os], RegisterFile].
	
% convert_d
instr(convert_d, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': convert_d'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [double(O)|Os], RegisterFile].

% convert_i
instr(convert_i, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': convert_i'),
	step_path_once(PI,NPI),   

	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	%toInt(O,Result),
	NewEE =.. [env, ScopeStack, [int(O)|Os], RegisterFile].
	
% convert_u
instr(convert_u, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': convert_u'),
	step_path_once(PI,NPI),   

	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	%toInt(O,Result),
	NewEE =.. [env, ScopeStack, [uint(O)|Os], RegisterFile].

% decrement
instr(decrement, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': decrement'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	% get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, ScopeStack, [toInt(O)-int(1)|Os], RegisterFile].

% decrement_i
instr(decrement_i, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': decrement_i'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	% get_property(Instr, next, NewInstr),	
   	NewEE =.. [env, ScopeStack, [toInt(O)-int(1)|Os], RegisterFile].
	
% deleteproperty
instr(deleteproperty, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': deleteproperty'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [Obj|Os], RegisterFile],
   	NewEE =.. [env, ScopeStack, [Value|Os], RegisterFile].

% divide
instr(divide, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):-
	write(WAST), writeln(': divide'),
	step_path_once(PI,NPI),   
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [toInt(V1) / toInt(V2) | OS] , RegisterFile].
	
% dup
instr(dup, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST):- 
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
   	NewEE =.. [env, ScopeStack, [O,O|Os], RegisterFile].	

% equals
instr(equals, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': equals'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(V1 == V2) | OS], RegisterFile].
    
% findproperty
instr(findproperty, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': findproperty'),
	step_path_once(PI,NPI),   

	EE =.. [env, ScopeStack, Os, RegisterFile],

	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,SC,Strings,NSC,Namespaces,_,_,MNC,Multinames)),
	nth(Index, Multinames, m_info(Kind, qname(MNNamespace, MNName))),

	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NoArgOpStack = [Obj | OpStack],

	nth(MNNamespace, Namespaces, namespace_info(_NSType,NSString)),
	nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName)),
	nth(MNName, Strings, string_info(_SC, _SLI, PropertyName)),

	find_scope_object(NSName, ScopeStack, Object),

	NewEE =.. [env, ScopeStack, [Object|Os], RegisterFile].

% findpropstrict
instr(findpropstrict, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': findpropstrict'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, Os, RegisterFile],

	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,_,_,_,_,_,_,MNC,Multinames)),
	nth(Index, Multinames, m_info(Kind, Data)),
	
	writeln('MULTINAME FOR FindPropStrict'),
	writeln(Kind),
	writeln(Data),

	writeln(ScopeStack),

	
	NewEE =.. [env, ScopeStack, [_Unbound|Os], RegisterFile].

% getlex
instr(getlex, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': getlex'),
	step_path_once(PI,NPI), 

	%PI =.. [path_info, TMN, TIC, _TempPath],
	%((TMN = 150, TIC = 5) -> spy(b_getval); true),
     
	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,SC,Strings,NSC,Namespaces,_,_,MNC,Multinames)),
	nth(Index, Multinames, m_info(Kind, MultiNameQ)),

	writeln(MultiNameQ),

	((MultiNameQ = qname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqnamel(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = multiname(MNName, MNNamespace)) -> true ; true),
	((MultiNameQ = multinamel(MNName, MNNamespace)) -> true ; true),

	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	%NoArgOpStack = [Obj | OpStack],

	%nth(MNNamespace, Namespaces, namespace_info(_NSType,NSString)),
	%nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName)),
	%nth(MNName, Strings, string_info(_SC, _SLI, PropertyName)),

	NewEE =.. [env, ScopeStack, [property(class(NSName),PropertyName)|OperandStack], RegisterFile].

% getlocal
instr(getlocal, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env,SS,OS,RF],
	ArgList = [Index],

	( (Index = 0) ->
		NewEE =.. [env, SS, [class('')|OS], RF]
	;
		nth0(Index, RF, Data),	
		NewEE =.. [env, SS, [Data|OS], RF]
	).
		
% getlocal_0
instr(getlocal_0, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env,SS,OS,RF],
	NewEE =.. [env, SS, [class('')|OS], RF].

% getlocal_1
instr(getlocal_1, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env,SS,OS,RF],
	nth0(1, RF, Data),	
	NewEE =.. [env, SS, [Data|OS], RF].	
	
% getlocal_2
instr(getlocal_2, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env,SS,OS,RF],
	nth0(2, RF, Data),	
	NewEE =.. [env, SS, [Data|OS], RF].

% getlocal_3
instr(getlocal_3, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env,SS,OS,RF],
	nth0(3, RF, Data),	
	NewEE =.. [env, SS, [Data|OS], RF].

% getglobalscope
instr(getglobalscope, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': getglobalscope'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	last(ScopeStack, GlobalScope),	
   	NewEE =.. [env, ScopeStack, [GlobalScope|OperandStack], RegisterFile].	

% getproperty
instr(getproperty, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': getproperty'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	ArgList = [_Index],
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% getscopeobject
% Index must be between 0 and ScopeDepth-1. Assuming that the bytecode loader
% takes care of that.
instr(getscopeobject, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	length(ScopeStack, ScopeDepth),
	NewIndex is (ScopeDepth - 1) - Index,
	nth0(NewIndex, ScopeStack, ScopeObject),	
   	NewEE =.. [env, ScopeStack, [ScopeObject|OperandStack], RegisterFile].	

% getslot
instr(getslot, [SlotIndex], state(H, [EE|EEs], _Trace, A), state(H, [NewEE|EEs], _Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': getslot'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [Object | OS], RegisterFile],
	writeln(Object),
	NewEE =.. [env, ScopeStack, [Value | OS], RegisterFile].

% getsuper
instr(getsuper, [SlotIndex], state(H, [EE|EEs], _Trace, A), state(H, [NewEE|EEs], _Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': getsuper'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [Object | OS], RegisterFile],
	writeln(Object),
	NewEE =.. [env, ScopeStack, [Value | OS], RegisterFile].

% greaterequals
instr(greaterequals, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [C1, C2 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(C1>=C2) | OS], RegisterFile].

% greaterthan
instr(greaterthan, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [C1, C2 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(C1>C2) | OS], RegisterFile].

% hasnext
instr(hasnext, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [C1, C2 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [Value | OS], RegisterFile].

% hasnext2
instr(hasnext2, [ObReg, IndReg], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, _WAST) :-

	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, OS, RegisterFile],
	NewEE =.. [env, ScopeStack, [Value | OS], RegisterFile].

% ----------------------
% CONDITIONAL BRANCHES
% ----------------------

% ifeq
instr(ifeq, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2 | OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=C2), (C1=\=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% iffalse
instr(iffalse, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, ((C1)=:=bool(false)), ((C1)=:=bool(true)), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% ifge
instr(ifge, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1>=C2), (C1<C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifgt
instr(ifgt, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1>C2), (C1=<C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifle
instr(ifle, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=<C2), (C1>C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% iflt
instr(iflt, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1<C2), (C1>=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifne
instr(ifne, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=C2), (C1=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifnge
instr(ifnge, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1<C2), (C1>=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% ifngt
instr(ifngt, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=<C2), (C1>C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% ifnle
instr(ifnle, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-

	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1>C2), (C1=<C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifnlt
instr(ifnlt, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1<C2), (C1>=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% ifstricteq
instr(ifstricteq, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-

	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=C2), (C1=\=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% ifstrictne
instr(ifstrictne, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-

	EE =.. [env, ScopeStack, [C1, C2| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=\=C2), (C1=C2), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% iftrue
instr(iftrue, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	
	EE =.. [env, ScopeStack, [C1| OS], RegisterFile],
	get_jump_path(PI, NPI, Offset, CL, NCL, (C1=bool(true)), (C1=bool(false)), WAST),
	NewEE =.. [env, ScopeStack, OS, RegisterFile].
	
% --------------------------
% END CONDITIONAL BRANCHES
% --------------------------

% in
instr(in, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A),  PI, NPI, CL, NCL, WAST) :-
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, [Name, Obj| OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(Value) | OS], RegisterFile].

% inclocal_i
instr(inclocal_i, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': inclocal_i'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, Os, RegisterFile],

	%nth0(Index, RegisterFile, Reg),
	


	NewEE =.. [env, ScopeStack, Os, RegisterFile].

% increment
instr(increment, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': increment'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [int(O)+int(1)|Os], RegisterFile].
	
% increment_i
instr(increment_i, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': increment_i'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	%toInt(O,X),
	NewEE =.. [env, ScopeStack, [int(X)+int(1)|Os], RegisterFile].


% initproperty
instr(initproperty, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': initproperty'),
	step_path_once(PI,NPI),   

	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,CP),
	CP =.. [cpoolinfo,_,_,_,_,_,_,_SC,Strings,_NSC,Namespaces,_,_,_MNC,Multinames],
	nth(Index, Multinames, m_info(Kind, MultiNameQ)),

	((MultiNameQ = qname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqname(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = rtqnamel(MNNamespace, MNName)) -> true ; true),
	((MultiNameQ = multiname(MNName, MNNamespace)) -> true ; true),
	((MultiNameQ = multinamel(MNName, MNNamespace)) -> true ; true),

	((MNNamespace = 0) ->
		NSName = '(*)'
	;
		nth(MNNamespace, Namespaces, namespace_info(_NSType,NSString)),
		%nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName)),
		((NSString = 0) ->
			NSName = ''
		;
			nth(NSString, Strings,  string_info(_SCNS, _SLINS, NSName))
		)
	),
	%((MNName = 0) ->
	%	MethodName = '(*)'
	%;
	%	nth(MNName, Strings, string_info(_SC, _SLI, MethodName))
	%),

		%		Data =.. [qname, I1, I2],


		%nth(I1, Namespaces, NS),
		%nth(I2, Strings, S),
	EE =.. [env, ScopeStack, [Value,Object|OperandStack], RegisterFile],


	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% istypelate
instr(istypelate, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': istypelate'),
	step_path_once(PI,NPI),   
	EE =.. [env, ScopeStack, [Value, Type|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(Value)|Os], RegisterFile].

% jump
instr(jump, [Offset], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	PI =.. [path_info, OMN, OIC, OP],
	
	% Do the branch
	b_getval(WAST, AST),
	abc_parser:getABC(method_bodies, AST, Methods),
	get_method2(OMN, Methods, Meth),
	Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,InsList,_EC1,_E1,_TC1,_T1],

	StartIC is (OIC+1),
	get_jump_target(Offset, StartIC, InsList, StartIC, NIC),
	NPI =.. [path_info, OMN, NIC, OP],

	writeln('JUMP:'),
	writeln(PI),
	writeln(NPI),
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% kill
instr(kill, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': kill'),
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	%	replace(Index, RegisterFile, Undefined, NewRegisterFile),
   	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].	

% label
instr(label, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': label'),
	step_path_once(PI,NPI), 
	  
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% greaterequals
instr(lessequals, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, NCL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [C1, C2 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(C1=<C2) | OS], RegisterFile].

% lessthan
instr(lessthan, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(V1 < V2) | OS], RegisterFile].


% lookupswitch
instr(lookupswitch, [DefaultOffset, CaseCount, CaseOffsets], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, [NC|CL], SwitchCount, WAST) :-
	PI =.. [path_info, OMN, OIC, OP],

	% Do the branch
	b_getval(WAST, AST),
	abc_parser:getABC(method_bodies, AST, Methods),
	get_method2(OMN, Methods, Meth),
	Meth =.. [method_body,_Method1,_MS1,_LC1,_ISD1,_MSD1,_CL1,InsList,_EC1,_E1,_TC1,_T1],

	((SwitchCount = 0) ->
		Offset = DefaultOffset
	;
		nth(SwitchCount, CaseOffsets, Offset)
	),

	get_jump_target(Offset, OIC, InsList, OIC, NIC),
	NPI =.. [path_info, OMN, NIC, 0],

	writeln('LUS:'),
	writeln(PI),
	writeln(NPI),

	EE =.. [env, ScopeStack, [Index | OS], RegisterFile],

	NC = (Index=SwitchCount),

	NewEE =.. [env, ScopeStack, OS, RegisterFile].

% lshift
instr(lshift, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': lshift'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	LS = V1 << V2,
	NewEE =.. [env, ScopeStack, [LS | OS] , RegisterFile].

% modulo
instr(modulo, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': modulo'),
	step_path_once(PI,NPI), 
	  
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [toInt(V1) * toInt(V2) | OS] , RegisterFile].

% multiply
instr(multiply, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': multiply'),
	step_path_once(PI,NPI), 
	  
	
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],


	NewEE =.. [env, ScopeStack, [mod(V1,V2) | OS] , RegisterFile].

% negate
instr(negate, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-

	step_path_once(PI,NPI), 
	  
    	EE =.. [env, ScopeStack, [N | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [not(N) | OS] , RegisterFile].

% nextvalue
instr(nextvalue, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': nextvalue'),
	step_path_once(PI,NPI), 
	  
    	EE =.. [env, ScopeStack, [Obj , Ind | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [Value | OS] , RegisterFile].

% newactivation
instr(newactivation, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': newactivation'),
	step_path_once(PI,NPI), 
	  
	EE =.. [env, ScopeStack, Os, RegisterFile],
	NewEE =.. [env, ScopeStack, [_Unbound|Os], RegisterFile].

% newarray
instr(newarray, [ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST):- 
	write(WAST), writeln(': newactivation'),
	step_path_once(PI,NPI), 

	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	chop_list_until_nth2(OperandStack, ArgCount, OpStack),
	
	NewEE =.. [env, ScopeStack, [array(Value)|OpStack], RegisterFile].

% newclass
instr(newclass, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': newclass'),
	step_path_once(PI,CPI), 
	ArgList = [Index],

	% Get the ClassInfo of the class that needs to be created
	b_getval(WAST, AST),
	abc_parser:getABC(classes,AST,Classes),
	% writeln(Classes),
	nth0(Index, Classes, Class),
	%writeln(Class),
        Class =.. [class_info, CInit, _TC, _Traits],

	PI =.. [path_info, _MN, _IN, Path],
	NPI =.. [path_info, CInit, 0, Path],

	writeln('newclass'),
	write('Creating Class From: '),
	writeln(PI),
	write('To Class: '),
	writeln(NPI),


	EE =.. [env, ScopeStack, Os, RegisterFile],
	NewEE =.. [env, ScopeStack, [CPI|Os], RegisterFile].



% newfunction
instr(newfunction, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': newfunction'),
	step_path_once(PI,NPI),
       	  
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, Os, RegisterFile].
   
% newobject
instr(newobject, [ArgCount], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': newobject'),
	step_path_once(PI,NPI),
       	  
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],

	%spy(chop_2),

	chop_2(ArgCount, OperandStack, OpStack, [], Properties),

	NewObj =.. [object | Properties],

	Os = [NewObj | OpStack],
	
   	NewEE =.. [env, ScopeStack, Os, RegisterFile].

% nextname
instr(nextname, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': nextname'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [Object, Index|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [name(Value)|Os], RegisterFile].

% not
instr(not, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, [not(O)|Os], RegisterFile].

% pop
instr(pop, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	((PI=path_info(399,153,0)) -> trace ; true),
	EE =.. [env, ScopeStack, [_O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, Os, RegisterFile].

% popscope
instr(popscope, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST):-   
	step_path_once(PI,NPI),
	EE =.. [env, [_S|Ss], OperandStack, RegisterFile],
   	NewEE =.. [env, Ss, OperandStack, RegisterFile].

% pushbyte
instr(pushbyte, [Byte], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST):-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NewEE =.. [env, ScopeStack, [Byte|OperandStack], RegisterFile].

% pushdouble
instr(pushdouble, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,Doubles,_SC,_Strings,_NSC,_Namespaces,_,_,_MNC,_Multinames)),
	nth(Index, Doubles, Double),

	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [double(Double)|Os], RegisterFile].

% pushfalse
instr(pushfalse, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [bool(false)|Os], RegisterFile].

% pushint
instr(pushint, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	% Get the Property from the Multiname Constant Pool
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,Ints,_,_,_,_D,_SC,_S,_NSC,_Ns,_,_,_MNC,_Mult)),
	nth(Index, Ints, Int),

	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [Int|Os], RegisterFile].

% pushnull
instr(pushnan, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile], 
   	NewEE =.. [env, ScopeStack, [nan|Os], RegisterFile].

% pushnull
instr(pushnull, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile], 
   	NewEE =.. [env, ScopeStack, [null|Os], RegisterFile].
	
% pushscope
instr(pushscope, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST):- 
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
   	NewEE =.. [env, [O|ScopeStack], Os, RegisterFile].
	
% pushshort
instr(pushshort, [Short], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [short(Short)|Os], RegisterFile].

% pushstring
instr(pushstring, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	% Get the Property from the Multiname Constant Pool
	%
	%spy(breakpoint_temp),
	%breakpoint_temp(br),
	b_getval(WAST, AST),
	abc_parser:getABC(constant_pool,AST,cpoolinfo(_,_,_,_,_,_,_SC,Strings,_NSC,_Namespaces,_,_,_MNC,_Multinames)),
	nth(Index, Strings, string_info(_SCNS, _SLINS, StrPush)),

	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [string(StrPush)|Os], RegisterFile].

% pushtrue
instr(pushtrue, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [bool(true)|Os], RegisterFile].

% pushundefined
instr(pushundefined, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, [undefined|Os], RegisterFile].

% pushwith
instr(pushwith, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST):- 
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
   	NewEE =.. [env, [O|ScopeStack], Os, RegisterFile].

% returnvalue
instr(returnvalue, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': returnvalue'),
	EE =.. [env, ScopeStack, [Goto, RV |Os], _RegisterFile],

	Goto =.. [path_info, MN, IC, P],
	PI =.. [path_info, _OMN, _OIC, OP],
	NPI =.. [path_info, MN, IC, OP],

	write('Returning from: '),
	writeln(Goto),
	write('To: '),
	writeln(Path),
	write('Returning: '), writeln(RV),

	NewEE =.. [env, ScopeStack, [RV | Os], _NewRegisterFile].

% returnvalue
instr(returnvalue, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [EE|EEs], Trace, A), PI, PI, CL, CL, _WAST) :-
	writeln('returnvalue hit with nowhere to return to...').

% returnvoid
%instr(returnvoid, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
%	EE =.. [env, ScopeStack, [], _RegisterFile],
%	writeln('ReturnVoid hit with nowhere to return to...').

% returnvoid
instr(returnvoid, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': returnvoid'),
	EE =.. [env, ScopeStack, [Path|Os], RegisterFile],
	NewEE =..  [env, ScopeStack, Os, RegisterFile],
	Path =.. [path_info, MN, IC, P],

	write('Returning from: '),
	writeln(PI),
	write('To: '),
	writeln(Path),

	PI =.. [path_info, _OMN, _OIC, OP],
	NPI =.. [path_info, MN, IC, OP].

% returnvoid
instr(returnvoid, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [EE|EEs], Trace, A), PI, PI, CL, CL, _WAST) :-
	writeln('ReturnVoid hit with nowhere to return to...').

% rshift
instr(rshift, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': rshift'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	RS = V2 >> V1,
	NewEE =.. [env, ScopeStack, [RS | OS] , RegisterFile].

% setlocal
instr(setlocal, ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': setlocal'),
	step_path_once(PI,NPI),
       	  
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	ArgList = [Index],
	replace(Index, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile].

% setlocal_0
instr(setlocal_0, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': setlocal_0'),	
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	replace(0, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile].
	
% setlocal_1
instr(setlocal_1, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': setlocal_1'),	
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	replace(1, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile].

% setlocal_2
instr(setlocal_2, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': setlocal_2'),
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	replace(2, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile].

% setlocal_3	
instr(setlocal_3, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :- 
	write(WAST), writeln(': setlocal_3'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [O|Os], RegisterFile],
	replace(3, RegisterFile, O, NewRegisterFile),
	NewEE =.. [env, ScopeStack, Os, NewRegisterFile].
	
% setproperty
instr(setproperty, [_Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': setproperty'),
	step_path_once(PI,NPI),
   	EE =.. [env, ScopeStack, OperandStack, RegisterFile],
	NewEE =.. [env, ScopeStack, OperandStack, RegisterFile].

% setslot
instr(setslot, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': setslot'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, Os, RegisterFile],
   	NewEE =.. [env, ScopeStack, Os, RegisterFile].

% setsuper
instr(setsuper, [Index], state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': setsuper'),
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [Obj|Os], RegisterFile],
   	NewEE =.. [env, ScopeStack, [Value|Os], RegisterFile].
    
% strictequals
instr(strictequals, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': strictequals'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [bool(V1=V2) | OS] , RegisterFile].

% subtract
instr(subtract, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, WAST) :-
	write(WAST), writeln(': subtract'),
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [toInt(V1) - toInt(V2) | OS] , RegisterFile].

% swap
instr(swap, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI), 
    	EE =.. [env, ScopeStack, [V2, V1 | OS], RegisterFile],
	NewEE =.. [env, ScopeStack, [V1, V2 | OS] , RegisterFile].

% throw
instr(throw, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI),
	EE =.. [env, ScopeStack, [_O|Os], RegisterFile],
	NewEE =.. [env, ScopeStack, Os, RegisterFile].

% typeof
instr(typeof, _ArgList, state(H, [EE|EEs], Trace, A), state(H, [NewEE|EEs], Trace, A), PI, NPI, CL, CL, _WAST) :-
	step_path_once(PI,NPI), 
	EE =.. [env, ScopeStack, [V | Os], RegisterFile],
   	NewEE =.. [env, ScopeStack, [string(V)|Os], RegisterFile].

find_scope_object(_Name, [], _Var).
find_scope_object(Name, [class(Name) | _ScopeStack], class(Name)).
find_scope_object(Name, [SO | SS], Obj) :-
	find_scope_object(Name, SS, Obj).

% toInt converts from one of the types either specified in the ECMA 262 document
% or in the AVM 2 Overview Document, whichever one is more specific to an int.
% currently assumes that we are dealing only with integers. For the rest,
% returns top.
toInt(undefined, undefined).
toInt(null, null).
toInt(bool(true), int(1)).
toInt(bool(false), int(0)).
toInt(int(Value),int(Value)).
toInt(int32(Value),int(Value)).
toInt(uint32(Value), int(Value)).
toInt(uint16(Value),int(Value)).
toInt(double(Value),int(Value)).
toInt(string(_Value),_Unbound).
toInt(object(_Value),_Unbound).
toInt(reference(_Value),_Unbound).
toInt(list(_Value),_Unbound).
toInt(completion(_Value),_Unbound).
toInt(namespace(Value), NewVal) :- 
	toInt(Value, NewVal).
    
isgreaterequals(int(V1), int(V2), bool(true)) :- V1 >= V2.
isgreaterequals(int(V1), int(V2), bool(false)) :- V1 < V2.
isgreaterequals(V1, V2, tt) :-
	V1 \= int(_X); V2 \= int(_Y).
    
isequals(int(V1), int(V1), bool(true)).
isequals(int(V1), int(V2), bool(false)) :- V1 =\= V2.
isequals(V1, V2, tt) :-
	V1 \= int(_X); V2 \= int(_Y).

help_ifeq(bool(true), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifeq(bool(false), Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifeq(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifeq(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
    
help_ifngt(bool(true), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_ifngt(bool(false), Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifngt(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_ifngt(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
    
help_iflt(bool(true), Instr, NewInstr) :- 
	get_property(Instr, next, NewInstr).
help_iflt(bool(false), Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
help_iflt(tt, Instr, NewInstr) :-
	get_property(Instr, next, NewInstr).
help_iflt(tt, Instr, NewInstr) :-
	get_property(Instr, jumplabel, NewInstr).
	
help_increment_i(int(R1), int(R2)) :- R2 is R1 + 1.
help_increment_i(_, tt).

/*
 * defined/1 is true if the argument is not a list and not top (tt),
 * or true if the argument is either an empty list or a list where
 * every element satisfies defined/1.
 */
defined([]).
defined([H|R]) :- 
	H \= tt, 
	defined(R).

% helper function for replacing the nth element in a list with the given 
% element. Index starts at 0, so it is really the (n-1)th element that 
% is being replaced.
%
replace(Index, OrigList, NewVal, NewList) :-
	nth0(Index, OrigList, _, L2),
	nth0(Index, NewList, NewVal, L2).

breakpoint_temp(br).

